t:, w:World, ln:IdLnk. 0<||queue(ln;t)||  mlnk(hd(queue(ln;t))) = ln 

latex

Definitions

Prop, t  T, P  Q, x:A. B(x), (x  l), P  Q, P & Q, S  T, Top, P  Q, , True, T, false, true, if b t else f fi, i  j < k, False, A, AB, {i..j}, {i...j}, A & B, x:A. B(x), Msg, ij, i<j, b, ij, Y, nth_tl(n;as), l[i], queue(l;t), Unit, , snds(l;t), onlnk(l;mss), m(l;t),

Lemmas

nat wf, world wf, IdLnk wf, w-queue wf, w-Msg wf, length wf1, l member wf, top wf, w-snds wf, le wf, w-rcvs wf, ldst wf, w-action wf, general length nth tl, non neg length, assert of le int, bnot of lt int, true wf, squash wf, eqff to assert, bnot wf, le int wf, assert of lt int, eqtt to assert, assert wf, iff transitivity, bool wf, lt int wf, select nth tl, select wf, upto wf, w-ml wf, int seg wf, map wf, member-concat, member map, mlnk wf, Id wf, w-M wf, Msg wf, lsrc wf, w-m wf, eq lnk wf, member filter, assert-eq-lnk, hd wf